Nuprl Lemma : sublist_append1
11,40
postcript
pdf
T
:Type,
L1
,
L2
:(
T
List).
L1
L1
@
L2
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
append
interleaving
,
append
wf
,
interleaving
sublist
origin
T:Type, L1, L2:(T List). L1 
L1 @ L2 T:Type, L1, L2:(T List). L1 L1 @ L2 
Tx:A. B(x)
Q